Termination proof of /tmp/tmpO_2rh8/CountMetaList.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 1230 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIDPv1Proof (⇒, 300 ms)

        ↳7 IDP

        ↳8 IDPNonInfProof (⇒, 1300 ms)

        ↳9 IDP

        ↳10 IDependencyGraphProof (⇔, 0 ms)

        ↳11 IDP

        ↳12 IDPNonInfProof (⇒, 80 ms)

        ↳13 IDP

        ↳14 IDependencyGraphProof (⇔, 0 ms)

        ↳15 TRUE

    ↳16 JBCTerminationSCC

        ↳17 SCCToIDPv1Proof (⇒, 1570 ms)

        ↳18 IDP

        ↳19 IDPtoQDPProof (⇒, 0 ms)

        ↳20 QDP

        ↳21 UsableRulesReductionPairsProof (⇔, 30 ms)

        ↳22 QDP

        ↳23 MRRProof (⇔, 0 ms)

        ↳24 QDP

        ↳25 PisEmptyProof (⇔, 0 ms)

        ↳26 YES

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: CountMetaList

public class CountMetaList {
	public static void main(String[] args) {
		Random.args = args;
		List l = createMetaList();

		int count = countMetaList(l);
	}

	public static int countMetaList(List cur) {
		int res = 0;
		while (cur != null) {
			if (cur.value instanceof List) {
				List inner = (List) cur.value;
				cur.value = inner.next;
				cur = new List(inner.value, cur);
			}
			cur = cur.next;
			res++;
		}

		return res;
	}

	public static List createMetaList() {
		int count = Random.random();
		List cur = null;
		for (int i = 0; i < count; i++) {
			int innerCount = Random.random();
			List innerList = null;
			for (int j = innerCount; j > 0; j--) {
				innerList = new List(null, innerList);
			}
			cur = new List(innerList, cur);
		}

		return cur;
	}
}

class List {
	Object value;
	List next;

	public List(Object v, List n) {
		this.value = v;
		this.next = n;
	}
}


public class Random {
  static String[] args;
  static int index = 0;

  public static int random() {
    String string = args[index];
    index++;
    return string.length();
  }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
CountMetaList.main([Ljava/lang/String;)V: Graph of 201 nodes with 1 SCC.

CountMetaList.createMetaList()LList;: Graph of 195 nodes with 1 SCC.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 2 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: CountMetaList.createMetaList()LList;
SCC calls the following helper methods:
Performed SCC analyses: UsedFieldsAnalysis

(6) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 69 rules for P and 0 rules for R.

P rules:
2361_0_createMetaList_Load(EOS(STATIC_2361), i77, i476, i476) → 2369_0_createMetaList_GE(EOS(STATIC_2369), i77, i476, i476, i77)
2369_0_createMetaList_GE(EOS(STATIC_2369), i77, i476, i476, i77) → 2377_0_createMetaList_GE(EOS(STATIC_2377), i77, i476, i476, i77)
2377_0_createMetaList_GE(EOS(STATIC_2377), i77, i476, i476, i77) → 2396_0_createMetaList_InvokeMethod(EOS(STATIC_2396), i77, i476) | <(i476, i77)
2396_0_createMetaList_InvokeMethod(EOS(STATIC_2396), i77, i476) → 2426_0_random_FieldAccess(EOS(STATIC_2426), i77, i476)
2426_0_random_FieldAccess(EOS(STATIC_2426), i77, i476) → 2453_0_random_FieldAccess(EOS(STATIC_2453), i77, i476)
2453_0_random_FieldAccess(EOS(STATIC_2453), i77, i476) → 2467_0_random_ArrayAccess(EOS(STATIC_2467), i77, i476)
2467_0_random_ArrayAccess(EOS(STATIC_2467), i77, i476) → 2476_0_random_ArrayAccess(EOS(STATIC_2476), i77, i476)
2476_0_random_ArrayAccess(EOS(STATIC_2476), i77, i476) → 2485_0_random_Store(EOS(STATIC_2485), i77, i476, o1984)
2485_0_random_Store(EOS(STATIC_2485), i77, i476, o1984) → 2496_0_random_FieldAccess(EOS(STATIC_2496), i77, i476, o1984)
2496_0_random_FieldAccess(EOS(STATIC_2496), i77, i476, o1984) → 2499_0_random_ConstantStackPush(EOS(STATIC_2499), i77, i476, o1984)
2499_0_random_ConstantStackPush(EOS(STATIC_2499), i77, i476, o1984) → 2505_0_random_IntArithmetic(EOS(STATIC_2505), i77, i476, o1984)
2505_0_random_IntArithmetic(EOS(STATIC_2505), i77, i476, o1984) → 2511_0_random_FieldAccess(EOS(STATIC_2511), i77, i476, o1984)
2511_0_random_FieldAccess(EOS(STATIC_2511), i77, i476, o1984) → 2516_0_random_Load(EOS(STATIC_2516), i77, i476, o1984)
2516_0_random_Load(EOS(STATIC_2516), i77, i476, o1984) → 2526_0_random_InvokeMethod(EOS(STATIC_2526), i77, i476, o1984)
2526_0_random_InvokeMethod(EOS(STATIC_2526), i77, i476, java.lang.Object(o2019sub)) → 2533_0_random_InvokeMethod(EOS(STATIC_2533), i77, i476, java.lang.Object(o2019sub))
2533_0_random_InvokeMethod(EOS(STATIC_2533), i77, i476, java.lang.Object(o2019sub)) → 2541_0_length_Load(EOS(STATIC_2541), i77, i476, java.lang.Object(o2019sub), java.lang.Object(o2019sub))
2541_0_length_Load(EOS(STATIC_2541), i77, i476, java.lang.Object(o2019sub), java.lang.Object(o2019sub)) → 2567_0_length_FieldAccess(EOS(STATIC_2567), i77, i476, java.lang.Object(o2019sub), java.lang.Object(o2019sub))
2567_0_length_FieldAccess(EOS(STATIC_2567), i77, i476, java.lang.Object(java.lang.String(o2111sub, i531)), java.lang.Object(java.lang.String(o2111sub, i531))) → 2587_0_length_FieldAccess(EOS(STATIC_2587), i77, i476, java.lang.Object(java.lang.String(o2111sub, i531)), java.lang.Object(java.lang.String(o2111sub, i531))) | &&(>=(i531, 0), >=(i532, 0))
2587_0_length_FieldAccess(EOS(STATIC_2587), i77, i476, java.lang.Object(java.lang.String(o2111sub, i531)), java.lang.Object(java.lang.String(o2111sub, i531))) → 2603_0_length_Return(EOS(STATIC_2603), i77, i476, java.lang.Object(java.lang.String(o2111sub, i531)), i531)
2603_0_length_Return(EOS(STATIC_2603), i77, i476, java.lang.Object(java.lang.String(o2111sub, i531)), i531) → 2618_0_random_Return(EOS(STATIC_2618), i77, i476, i531)
2618_0_random_Return(EOS(STATIC_2618), i77, i476, i531) → 2629_0_createMetaList_Store(EOS(STATIC_2629), i77, i476, i531)
2629_0_createMetaList_Store(EOS(STATIC_2629), i77, i476, i531) → 2640_0_createMetaList_ConstantStackPush(EOS(STATIC_2640), i77, i476, i531)
2640_0_createMetaList_ConstantStackPush(EOS(STATIC_2640), i77, i476, i531) → 2650_0_createMetaList_Store(EOS(STATIC_2650), i77, i476, i531)
2650_0_createMetaList_Store(EOS(STATIC_2650), i77, i476, i531) → 2662_0_createMetaList_Load(EOS(STATIC_2662), i77, i476, i531)
2662_0_createMetaList_Load(EOS(STATIC_2662), i77, i476, i531) → 2669_0_createMetaList_Store(EOS(STATIC_2669), i77, i476, i531)
2669_0_createMetaList_Store(EOS(STATIC_2669), i77, i476, i531) → 2678_0_createMetaList_Load(EOS(STATIC_2678), i77, i476, i531)
2678_0_createMetaList_Load(EOS(STATIC_2678), i77, i476, i531) → 2935_0_createMetaList_Load(EOS(STATIC_2935), i77, i476, i531)
2935_0_createMetaList_Load(EOS(STATIC_2935), i77, i476, i603) → 2941_0_createMetaList_LE(EOS(STATIC_2941), i77, i476, i603, i603)
2941_0_createMetaList_LE(EOS(STATIC_2941), i77, i476, matching1, matching2) → 2946_0_createMetaList_LE(EOS(STATIC_2946), i77, i476, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
2941_0_createMetaList_LE(EOS(STATIC_2941), i77, i476, i608, i608) → 2947_0_createMetaList_LE(EOS(STATIC_2947), i77, i476, i608, i608)
2946_0_createMetaList_LE(EOS(STATIC_2946), i77, i476, matching1, matching2) → 2951_0_createMetaList_New(EOS(STATIC_2951), i77, i476) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
2951_0_createMetaList_New(EOS(STATIC_2951), i77, i476) → 2954_0_createMetaList_Duplicate(EOS(STATIC_2954), i77, i476)
2954_0_createMetaList_Duplicate(EOS(STATIC_2954), i77, i476) → 2959_0_createMetaList_Load(EOS(STATIC_2959), i77, i476)
2959_0_createMetaList_Load(EOS(STATIC_2959), i77, i476) → 2965_0_createMetaList_Load(EOS(STATIC_2965), i77, i476)
2965_0_createMetaList_Load(EOS(STATIC_2965), i77, i476) → 2972_0_createMetaList_InvokeMethod(EOS(STATIC_2972), i77, i476)
2972_0_createMetaList_InvokeMethod(EOS(STATIC_2972), i77, i476) → 2976_0_<init>_Load(EOS(STATIC_2976), i77, i476)
2976_0_<init>_Load(EOS(STATIC_2976), i77, i476) → 2988_0_<init>_InvokeMethod(EOS(STATIC_2988), i77, i476)
2988_0_<init>_InvokeMethod(EOS(STATIC_2988), i77, i476) → 2995_0_<init>_Load(EOS(STATIC_2995), i77, i476)
2995_0_<init>_Load(EOS(STATIC_2995), i77, i476) → 3002_0_<init>_Load(EOS(STATIC_3002), i77, i476)
3002_0_<init>_Load(EOS(STATIC_3002), i77, i476) → 3009_0_<init>_FieldAccess(EOS(STATIC_3009), i77, i476)
3009_0_<init>_FieldAccess(EOS(STATIC_3009), i77, i476) → 3019_0_<init>_Load(EOS(STATIC_3019), i77, i476)
3019_0_<init>_Load(EOS(STATIC_3019), i77, i476) → 3028_0_<init>_Load(EOS(STATIC_3028), i77, i476)
3028_0_<init>_Load(EOS(STATIC_3028), i77, i476) → 3036_0_<init>_FieldAccess(EOS(STATIC_3036), i77, i476)
3036_0_<init>_FieldAccess(EOS(STATIC_3036), i77, i476) → 3044_0_<init>_Return(EOS(STATIC_3044), i77, i476)
3044_0_<init>_Return(EOS(STATIC_3044), i77, i476) → 3052_0_createMetaList_Store(EOS(STATIC_3052), i77, i476)
3052_0_createMetaList_Store(EOS(STATIC_3052), i77, i476) → 3062_0_createMetaList_Inc(EOS(STATIC_3062), i77, i476)
3062_0_createMetaList_Inc(EOS(STATIC_3062), i77, i476) → 3066_0_createMetaList_JMP(EOS(STATIC_3066), i77, +(i476, 1)) | >=(i476, 0)
3066_0_createMetaList_JMP(EOS(STATIC_3066), i77, i618) → 3072_0_createMetaList_Load(EOS(STATIC_3072), i77, i618)
3072_0_createMetaList_Load(EOS(STATIC_3072), i77, i618) → 2354_0_createMetaList_Load(EOS(STATIC_2354), i77, i618)
2354_0_createMetaList_Load(EOS(STATIC_2354), i77, i476) → 2361_0_createMetaList_Load(EOS(STATIC_2361), i77, i476, i476)
2947_0_createMetaList_LE(EOS(STATIC_2947), i77, i476, i608, i608) → 2952_0_createMetaList_New(EOS(STATIC_2952), i77, i476, i608) | >(i608, 0)
2952_0_createMetaList_New(EOS(STATIC_2952), i77, i476, i608) → 2955_0_createMetaList_Duplicate(EOS(STATIC_2955), i77, i476, i608)
2955_0_createMetaList_Duplicate(EOS(STATIC_2955), i77, i476, i608) → 2961_0_createMetaList_ConstantStackPush(EOS(STATIC_2961), i77, i476, i608)
2961_0_createMetaList_ConstantStackPush(EOS(STATIC_2961), i77, i476, i608) → 2967_0_createMetaList_Load(EOS(STATIC_2967), i77, i476, i608)
2967_0_createMetaList_Load(EOS(STATIC_2967), i77, i476, i608) → 2973_0_createMetaList_InvokeMethod(EOS(STATIC_2973), i77, i476, i608)
2973_0_createMetaList_InvokeMethod(EOS(STATIC_2973), i77, i476, i608) → 2978_0_<init>_Load(EOS(STATIC_2978), i77, i476, i608)
2978_0_<init>_Load(EOS(STATIC_2978), i77, i476, i608) → 2990_0_<init>_InvokeMethod(EOS(STATIC_2990), i77, i476, i608)
2990_0_<init>_InvokeMethod(EOS(STATIC_2990), i77, i476, i608) → 2996_0_<init>_Load(EOS(STATIC_2996), i77, i476, i608)
2996_0_<init>_Load(EOS(STATIC_2996), i77, i476, i608) → 3004_0_<init>_Load(EOS(STATIC_3004), i77, i476, i608)
3004_0_<init>_Load(EOS(STATIC_3004), i77, i476, i608) → 3011_0_<init>_FieldAccess(EOS(STATIC_3011), i77, i476, i608)
3011_0_<init>_FieldAccess(EOS(STATIC_3011), i77, i476, i608) → 3021_0_<init>_Load(EOS(STATIC_3021), i77, i476, i608)
3021_0_<init>_Load(EOS(STATIC_3021), i77, i476, i608) → 3030_0_<init>_Load(EOS(STATIC_3030), i77, i476, i608)
3030_0_<init>_Load(EOS(STATIC_3030), i77, i476, i608) → 3037_0_<init>_FieldAccess(EOS(STATIC_3037), i77, i476, i608)
3037_0_<init>_FieldAccess(EOS(STATIC_3037), i77, i476, i608) → 3046_0_<init>_Return(EOS(STATIC_3046), i77, i476, i608)
3046_0_<init>_Return(EOS(STATIC_3046), i77, i476, i608) → 3053_0_createMetaList_Store(EOS(STATIC_3053), i77, i476, i608)
3053_0_createMetaList_Store(EOS(STATIC_3053), i77, i476, i608) → 3064_0_createMetaList_Inc(EOS(STATIC_3064), i77, i476, i608)
3064_0_createMetaList_Inc(EOS(STATIC_3064), i77, i476, i608) → 3068_0_createMetaList_JMP(EOS(STATIC_3068), i77, i476, +(i608, -1)) | >(i608, 0)
3068_0_createMetaList_JMP(EOS(STATIC_3068), i77, i476, i619) → 3074_0_createMetaList_Load(EOS(STATIC_3074), i77, i476, i619)
3074_0_createMetaList_Load(EOS(STATIC_3074), i77, i476, i619) → 2935_0_createMetaList_Load(EOS(STATIC_2935), i77, i476, i619)
R rules:

Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.

P rules:
2941_0_createMetaList_LE(EOS(STATIC_2941), x0, x1, 0, 0) → 2941_0_createMetaList_LE(EOS(STATIC_2941), x0, +(x1, 1), x4, x4) | &&(&&(>(+(x4, 1), 0), >(+(x1, 1), 0)), >(x0, +(x1, 1)))
2941_0_createMetaList_LE(EOS(STATIC_2941), x0, x1, x2, x2) → 2941_0_createMetaList_LE(EOS(STATIC_2941), x0, x1, +(x2, -1), +(x2, -1)) | >(x2, 0)
R rules:

Filtered ground terms:

2941_0_createMetaList_LE(x1, x2, x3, x4, x5) → 2941_0_createMetaList_LE(x2, x3, x4, x5)
EOS(x1) → EOS
Cond_2941_0_createMetaList_LE1(x1, x2, x3, x4, x5, x6) → Cond_2941_0_createMetaList_LE1(x1, x3, x4, x5, x6)
Cond_2941_0_createMetaList_LE(x1, x2, x3, x4, x5, x6, x7) → Cond_2941_0_createMetaList_LE(x1, x3, x4, x7)

Filtered duplicate args:

2941_0_createMetaList_LE(x1, x2, x3, x4) → 2941_0_createMetaList_LE(x1, x2, x4)
Cond_2941_0_createMetaList_LE1(x1, x2, x3, x4, x5) → Cond_2941_0_createMetaList_LE1(x1, x2, x3, x5)

Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.

P rules:
2941_0_createMetaList_LE(x0, x1, 0) → 2941_0_createMetaList_LE(x0, +(x1, 1), x4) | &&(&&(>(x4, -1), >(x1, -1)), >(x0, +(x1, 1)))
2941_0_createMetaList_LE(x0, x1, x2) → 2941_0_createMetaList_LE(x0, x1, +(x2, -1)) | >(x2, 0)
R rules:

Finished conversion. Obtained 4 rules for P and 0 rules for R. System has predefined symbols.

P rules:
2941_0_CREATEMETALIST_LE(x0, x1, 0) → COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4, -1), >(x1, -1)), >(x0, +(x1, 1))), x0, x1, 0, x4)
COND_2941_0_CREATEMETALIST_LE(TRUE, x0, x1, 0, x4) → 2941_0_CREATEMETALIST_LE(x0, +(x1, 1), x4)
2941_0_CREATEMETALIST_LE(x0, x1, x2) → COND_2941_0_CREATEMETALIST_LE1(>(x2, 0), x0, x1, x2)
COND_2941_0_CREATEMETALIST_LE1(TRUE, x0, x1, x2) → 2941_0_CREATEMETALIST_LE(x0, x1, +(x2, -1))
R rules:

(7) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 2941_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2941_0_CREATEMETALIST_LE(x4[0] > -1 && x1[0] > -1 && x0[0] > x1[0] + 1, x0[0], x1[0], 0, x4[0])
(1): COND_2941_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2941_0_CREATEMETALIST_LE(x0[1], x1[1] + 1, x4[1])
(2): 2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(x2[2] > 0, x0[2], x1[2], x2[2])
(3): COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2941_0_CREATEMETALIST_LE(x0[3], x1[3], x2[3] + -1)

(0) -> (1), if (x4[0] > -1 && x1[0] > -1 && x0[0] > x1[0] + 1 ∧x0[0] →^* x0[1]∧x1[0] →^* x1[1]∧x4[0] →^* x4[1])

(1) -> (0), if (x0[1] →^* x0[0]∧x1[1] + 1 →^* x1[0]∧x4[1] →^* 0)

(1) -> (2), if (x0[1] →^* x0[2]∧x1[1] + 1 →^* x1[2]∧x4[1] →^* x2[2])

(2) -> (3), if (x2[2] > 0 ∧x0[2] →^* x0[3]∧x1[2] →^* x1[3]∧x2[2] →^* x2[3])

(3) -> (0), if (x0[3] →^* x0[0]∧x1[3] →^* x1[0]∧x2[3] + -1 →^* 0)

(3) -> (2), if (x0[3] →^* x0[2]∧x1[3] →^* x1[2]∧x2[3] + -1 →^* x2[2])

The set Q is empty.

(8) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpDefaultShapeHeuristic@1bec079e Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 1 Max Right Steps: 1

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair 2941_0_CREATEMETALIST_LE(x0, x1, 0) → COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4, -1), >(x1, -1)), >(x0, +(x1, 1))), x0, x1, 0, x4) the following chains were created:

We consider the chain COND_2941_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1]), 2941_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0]), COND_2941_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1]) which results in the following constraint:
(1)    (x0[1]=x0[0]∧+(x1[1], 1)=x1[0]∧x4[1]=0∧&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1)))=TRUE∧x0[0]=x0[1]1∧x1[0]=x1[1]1∧x4[0]=x4[1]1 ⇒ 2941_0_CREATEMETALIST_LE(x0[0], x1[0], 0)≥NonInfC∧2941_0_CREATEMETALIST_LE(x0[0], x1[0], 0)≥COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])∧(U^Increasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥))

We simplified constraint (1) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(2)    (>(x0[0], +(+(x1[1], 1), 1))=TRUE∧>(x4[0], -1)=TRUE∧>(+(x1[1], 1), -1)=TRUE ⇒ 2941_0_CREATEMETALIST_LE(x0[0], +(x1[1], 1), 0)≥NonInfC∧2941_0_CREATEMETALIST_LE(x0[0], +(x1[1], 1), 0)≥COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(+(x1[1], 1), -1)), >(x0[0], +(+(x1[1], 1), 1))), x0[0], +(x1[1], 1), 0, x4[0])∧(U^Increasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x0[0] + [-3] + [-1]x1[1] ≥ 0∧x4[0] ≥ 0∧x1[1] + [1] ≥ 0 ⇒ (U^Increasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[(-2)bni_20 + (-1)Bound*bni_20] + [(-1)bni_20]x1[1] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x0[0] + [-3] + [-1]x1[1] ≥ 0∧x4[0] ≥ 0∧x1[1] + [1] ≥ 0 ⇒ (U^Increasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[(-2)bni_20 + (-1)Bound*bni_20] + [(-1)bni_20]x1[1] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x0[0] + [-3] + [-1]x1[1] ≥ 0∧x4[0] ≥ 0∧x1[1] + [1] ≥ 0 ⇒ (U^Increasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[(-2)bni_20 + (-1)Bound*bni_20] + [(-1)bni_20]x1[1] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)

We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(6)    (x0[0] ≥ 0∧x4[0] ≥ 0∧x1[1] + [1] ≥ 0 ⇒ (U^Increasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)

We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
(7)    (x0[0] ≥ 0∧x4[0] ≥ 0∧[-1]x1[1] + [1] ≥ 0∧x1[1] ≥ 0 ⇒ (U^Increasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)

(8)    (x0[0] ≥ 0∧x4[0] ≥ 0∧x1[1] + [1] ≥ 0∧x1[1] ≥ 0 ⇒ (U^Increasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)
We consider the chain COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1)), 2941_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0]), COND_2941_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1]) which results in the following constraint:
(9)    (x0[3]=x0[0]∧x1[3]=x1[0]∧+(x2[3], -1)=0∧&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1)))=TRUE∧x0[0]=x0[1]∧x1[0]=x1[1]∧x4[0]=x4[1] ⇒ 2941_0_CREATEMETALIST_LE(x0[0], x1[0], 0)≥NonInfC∧2941_0_CREATEMETALIST_LE(x0[0], x1[0], 0)≥COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])∧(U^Increasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥))

We simplified constraint (9) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(10)    (+(x2[3], -1)=0∧>(x0[0], +(x1[0], 1))=TRUE∧>(x4[0], -1)=TRUE∧>(x1[0], -1)=TRUE ⇒ 2941_0_CREATEMETALIST_LE(x0[0], x1[0], 0)≥NonInfC∧2941_0_CREATEMETALIST_LE(x0[0], x1[0], 0)≥COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])∧(U^Increasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥))

We simplified constraint (10) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(11)    (x2[3] + [-1] ≥ 0∧x0[0] + [-2] + [-1]x1[0] ≥ 0∧x4[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[(-1)bni_20 + (-1)Bound*bni_20] + [(-1)bni_20]x1[0] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)

We simplified constraint (11) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(12)    (x2[3] + [-1] ≥ 0∧x0[0] + [-2] + [-1]x1[0] ≥ 0∧x4[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[(-1)bni_20 + (-1)Bound*bni_20] + [(-1)bni_20]x1[0] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)

We simplified constraint (12) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(13)    (x2[3] + [-1] ≥ 0∧x0[0] + [-2] + [-1]x1[0] ≥ 0∧x4[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[(-1)bni_20 + (-1)Bound*bni_20] + [(-1)bni_20]x1[0] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)

We simplified constraint (13) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(14)    (x2[3] + [-1] ≥ 0∧x0[0] ≥ 0∧x4[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)

For Pair COND_2941_0_CREATEMETALIST_LE(TRUE, x0, x1, 0, x4) → 2941_0_CREATEMETALIST_LE(x0, +(x1, 1), x4) the following chains were created:

We consider the chain 2941_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0]), COND_2941_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1]), 2941_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0]) which results in the following constraint:
(15)    (&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1)))=TRUE∧x0[0]=x0[1]∧x1[0]=x1[1]∧x4[0]=x4[1]∧x0[1]=x0[0]1∧+(x1[1], 1)=x1[0]1∧x4[1]=0 ⇒ COND_2941_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1])≥NonInfC∧COND_2941_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1])≥2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])∧(U^Increasing(2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥))

We simplified constraint (15) using rules (III), (IV), (IDP_CONSTANT_FOLD), (DELETE_TRIVIAL_REDUCESTO), (IDP_BOOLEAN) which results in the following new constraint:
(16)    (>(x0[0], +(x1[0], 1))=TRUE∧>(x1[0], -1)=TRUE ⇒ COND_2941_0_CREATEMETALIST_LE(TRUE, x0[0], x1[0], 0, 0)≥NonInfC∧COND_2941_0_CREATEMETALIST_LE(TRUE, x0[0], x1[0], 0, 0)≥2941_0_CREATEMETALIST_LE(x0[0], +(x1[0], 1), 0)∧(U^Increasing(2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥))

We simplified constraint (16) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(17)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-1)bni_22]x1[0] + [bni_22]x0[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)

We simplified constraint (17) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(18)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-1)bni_22]x1[0] + [bni_22]x0[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)

We simplified constraint (18) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(19)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-1)bni_22]x1[0] + [bni_22]x0[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)

We simplified constraint (19) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(20)    (x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥)∧[bni_22 + (-1)Bound*bni_22] + [bni_22]x0[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)
We consider the chain 2941_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0]), COND_2941_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1]), 2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]) which results in the following constraint:
(21)    (&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1)))=TRUE∧x0[0]=x0[1]∧x1[0]=x1[1]∧x4[0]=x4[1]∧x0[1]=x0[2]∧+(x1[1], 1)=x1[2]∧x4[1]=x2[2] ⇒ COND_2941_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1])≥NonInfC∧COND_2941_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1])≥2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])∧(U^Increasing(2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥))

We simplified constraint (21) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(22)    (>(x0[0], +(x1[0], 1))=TRUE∧>(x4[0], -1)=TRUE∧>(x1[0], -1)=TRUE ⇒ COND_2941_0_CREATEMETALIST_LE(TRUE, x0[0], x1[0], 0, x4[0])≥NonInfC∧COND_2941_0_CREATEMETALIST_LE(TRUE, x0[0], x1[0], 0, x4[0])≥2941_0_CREATEMETALIST_LE(x0[0], +(x1[0], 1), x4[0])∧(U^Increasing(2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥))

We simplified constraint (22) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(23)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x4[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-1)bni_22]x1[0] + [bni_22]x0[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)

We simplified constraint (23) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(24)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x4[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-1)bni_22]x1[0] + [bni_22]x0[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)

We simplified constraint (24) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(25)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x4[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-1)bni_22]x1[0] + [bni_22]x0[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)

We simplified constraint (25) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(26)    (x0[0] ≥ 0∧x4[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥)∧[bni_22 + (-1)Bound*bni_22] + [bni_22]x0[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)

For Pair 2941_0_CREATEMETALIST_LE(x0, x1, x2) → COND_2941_0_CREATEMETALIST_LE1(>(x2, 0), x0, x1, x2) the following chains were created:

We consider the chain 2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]), COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1)) which results in the following constraint:
(27)    (>(x2[2], 0)=TRUE∧x0[2]=x0[3]∧x1[2]=x1[3]∧x2[2]=x2[3] ⇒ 2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥NonInfC∧2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])∧(U^Increasing(COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥))

We simplified constraint (27) using rule (IV) which results in the following new constraint:
(28)    (>(x2[2], 0)=TRUE ⇒ 2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥NonInfC∧2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])∧(U^Increasing(COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥))

We simplified constraint (28) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(29)    (x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]x1[2] + [bni_24]x0[2] ≥ 0∧[(-1)bso_25] ≥ 0)

We simplified constraint (29) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(30)    (x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]x1[2] + [bni_24]x0[2] ≥ 0∧[(-1)bso_25] ≥ 0)

We simplified constraint (30) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(31)    (x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]x1[2] + [bni_24]x0[2] ≥ 0∧[(-1)bso_25] ≥ 0)

We simplified constraint (31) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(32)    (x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧[(-1)bni_24] = 0∧[bni_24] = 0∧[(-1)bni_24 + (-1)Bound*bni_24] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_25] ≥ 0)

We simplified constraint (32) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(33)    (x2[2] ≥ 0 ⇒ (U^Increasing(COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧[(-1)bni_24] = 0∧[bni_24] = 0∧[(-1)bni_24 + (-1)Bound*bni_24] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_25] ≥ 0)

For Pair COND_2941_0_CREATEMETALIST_LE1(TRUE, x0, x1, x2) → 2941_0_CREATEMETALIST_LE(x0, x1, +(x2, -1)) the following chains were created:

We consider the chain 2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]), COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1)), 2941_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0]) which results in the following constraint:
(34)    (>(x2[2], 0)=TRUE∧x0[2]=x0[3]∧x1[2]=x1[3]∧x2[2]=x2[3]∧x0[3]=x0[0]∧x1[3]=x1[0]∧+(x2[3], -1)=0 ⇒ COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3])≥NonInfC∧COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3])≥2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))∧(U^Increasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥))

We simplified constraint (34) using rules (III), (IV) which results in the following new constraint:
(35)    (>(x2[2], 0)=TRUE∧+(x2[2], -1)=0 ⇒ COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[2], x1[2], x2[2])≥NonInfC∧COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[2], x1[2], x2[2])≥2941_0_CREATEMETALIST_LE(x0[2], x1[2], +(x2[2], -1))∧(U^Increasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥))

We simplified constraint (35) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(36)    (x2[2] + [-1] ≥ 0∧x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x1[2] + [bni_26]x0[2] ≥ 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (36) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(37)    (x2[2] + [-1] ≥ 0∧x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x1[2] + [bni_26]x0[2] ≥ 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (37) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(38)    (x2[2] + [-1] ≥ 0∧x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x1[2] + [bni_26]x0[2] ≥ 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (38) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(39)    (x2[2] + [-1] ≥ 0∧x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26] = 0∧[bni_26] = 0∧[(-1)bni_26 + (-1)Bound*bni_26] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (39) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(40)    (x2[2] ≥ 0∧x2[2] ≥ 0 ⇒ (U^Increasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26] = 0∧[bni_26] = 0∧[(-1)bni_26 + (-1)Bound*bni_26] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)
We consider the chain 2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]), COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1)), 2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]) which results in the following constraint:
(41)    (>(x2[2], 0)=TRUE∧x0[2]=x0[3]∧x1[2]=x1[3]∧x2[2]=x2[3]∧x0[3]=x0[2]1∧x1[3]=x1[2]1∧+(x2[3], -1)=x2[2]1 ⇒ COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3])≥NonInfC∧COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3])≥2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))∧(U^Increasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥))

We simplified constraint (41) using rules (III), (IV) which results in the following new constraint:
(42)    (>(x2[2], 0)=TRUE ⇒ COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[2], x1[2], x2[2])≥NonInfC∧COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[2], x1[2], x2[2])≥2941_0_CREATEMETALIST_LE(x0[2], x1[2], +(x2[2], -1))∧(U^Increasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥))

We simplified constraint (42) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(43)    (x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x1[2] + [bni_26]x0[2] ≥ 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (43) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(44)    (x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x1[2] + [bni_26]x0[2] ≥ 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (44) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(45)    (x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x1[2] + [bni_26]x0[2] ≥ 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (45) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(46)    (x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26] = 0∧[bni_26] = 0∧[(-1)bni_26 + (-1)Bound*bni_26] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (46) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(47)    (x2[2] ≥ 0 ⇒ (U^Increasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26] = 0∧[bni_26] = 0∧[(-1)bni_26 + (-1)Bound*bni_26] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

2941_0_CREATEMETALIST_LE(x0, x1, 0) → COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4, -1), >(x1, -1)), >(x0, +(x1, 1))), x0, x1, 0, x4)
- (x0[0] ≥ 0∧x4[0] ≥ 0∧[-1]x1[1] + [1] ≥ 0∧x1[1] ≥ 0 ⇒ (U^Increasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)
- (x0[0] ≥ 0∧x4[0] ≥ 0∧x1[1] + [1] ≥ 0∧x1[1] ≥ 0 ⇒ (U^Increasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)
- (x2[3] + [-1] ≥ 0∧x0[0] ≥ 0∧x4[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)
COND_2941_0_CREATEMETALIST_LE(TRUE, x0, x1, 0, x4) → 2941_0_CREATEMETALIST_LE(x0, +(x1, 1), x4)
- (x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥)∧[bni_22 + (-1)Bound*bni_22] + [bni_22]x0[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)
- (x0[0] ≥ 0∧x4[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥)∧[bni_22 + (-1)Bound*bni_22] + [bni_22]x0[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)
2941_0_CREATEMETALIST_LE(x0, x1, x2) → COND_2941_0_CREATEMETALIST_LE1(>(x2, 0), x0, x1, x2)
- (x2[2] ≥ 0 ⇒ (U^Increasing(COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧[(-1)bni_24] = 0∧[bni_24] = 0∧[(-1)bni_24 + (-1)Bound*bni_24] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_25] ≥ 0)
COND_2941_0_CREATEMETALIST_LE1(TRUE, x0, x1, x2) → 2941_0_CREATEMETALIST_LE(x0, x1, +(x2, -1))
- (x2[2] ≥ 0∧x2[2] ≥ 0 ⇒ (U^Increasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26] = 0∧[bni_26] = 0∧[(-1)bni_26 + (-1)Bound*bni_26] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)
- (x2[2] ≥ 0 ⇒ (U^Increasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26] = 0∧[bni_26] = 0∧[(-1)bni_26 + (-1)Bound*bni_26] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0
POL(FALSE) = 0
POL(2941_0_CREATEMETALIST_LE(x₁, x₂, x₃)) = [-1] + [-1]x₂ + x₁
POL(0) = 0
POL(COND_2941_0_CREATEMETALIST_LE(x₁, x₂, x₃, x₄, x₅)) = [-1] + [-1]x₄ + [-1]x₃ + x₂ + [-1]x₁
POL(&&(x₁, x₂)) = 0
POL(>(x₁, x₂)) = [-1]
POL(-1) = [-1]
POL(+(x₁, x₂)) = x₁ + x₂
POL(1) = [1]
POL(COND_2941_0_CREATEMETALIST_LE1(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃ + x₂

The following pairs are in P_>:

COND_2941_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])

The following pairs are in P_bound:

2941_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])
COND_2941_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])

The following pairs are in P_≥:

2941_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])
2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])
COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))

At least the following rules have been oriented under context sensitive arithmetic replacement:

&&(TRUE, TRUE)¹ ↔ TRUE¹
&&(TRUE, FALSE)¹ ↔ FALSE¹
&&(FALSE, TRUE)¹ ↔ FALSE¹
&&(FALSE, FALSE)¹ ↔ FALSE¹

(9) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 2941_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2941_0_CREATEMETALIST_LE(x4[0] > -1 && x1[0] > -1 && x0[0] > x1[0] + 1, x0[0], x1[0], 0, x4[0])
(2): 2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(x2[2] > 0, x0[2], x1[2], x2[2])
(3): COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2941_0_CREATEMETALIST_LE(x0[3], x1[3], x2[3] + -1)

(3) -> (0), if (x0[3] →^* x0[0]∧x1[3] →^* x1[0]∧x2[3] + -1 →^* 0)

(3) -> (2), if (x0[3] →^* x0[2]∧x1[3] →^* x1[2]∧x2[3] + -1 →^* x2[2])

(2) -> (3), if (x2[2] > 0 ∧x0[2] →^* x0[3]∧x1[2] →^* x1[3]∧x2[2] →^* x2[3])

The set Q is empty.

(10) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(11) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(3): COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2941_0_CREATEMETALIST_LE(x0[3], x1[3], x2[3] + -1)
(2): 2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(x2[2] > 0, x0[2], x1[2], x2[2])

(3) -> (2), if (x0[3] →^* x0[2]∧x1[3] →^* x1[2]∧x2[3] + -1 →^* x2[2])

(2) -> (3), if (x2[2] > 0 ∧x0[2] →^* x0[3]∧x1[2] →^* x1[3]∧x2[2] →^* x2[3])

The set Q is empty.

(12) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpDefaultShapeHeuristic@1bec079e Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 1 Max Right Steps: 1

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1)) the following chains were created:

We consider the chain 2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]), COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1)), 2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]) which results in the following constraint:
(1)    (>(x2[2], 0)=TRUE∧x0[2]=x0[3]∧x1[2]=x1[3]∧x2[2]=x2[3]∧x0[3]=x0[2]1∧x1[3]=x1[2]1∧+(x2[3], -1)=x2[2]1 ⇒ COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3])≥NonInfC∧COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3])≥2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))∧(U^Increasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥))

We simplified constraint (1) using rules (III), (IV) which results in the following new constraint:
(2)    (>(x2[2], 0)=TRUE ⇒ COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[2], x1[2], x2[2])≥NonInfC∧COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[2], x1[2], x2[2])≥2941_0_CREATEMETALIST_LE(x0[2], x1[2], +(x2[2], -1))∧(U^Increasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [bni_13]x2[2] ≥ 0∧[1 + (-1)bso_14] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [bni_13]x2[2] ≥ 0∧[1 + (-1)bso_14] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [bni_13]x2[2] ≥ 0∧[1 + (-1)bso_14] ≥ 0)

We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(6)    (x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧0 = 0∧0 = 0∧[(-1)bni_13 + (-1)Bound*bni_13] + [bni_13]x2[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_14] ≥ 0)

We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(7)    (x2[2] ≥ 0 ⇒ (U^Increasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_13] + [bni_13]x2[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_14] ≥ 0)

For Pair 2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]) the following chains were created:

We consider the chain 2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]), COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1)) which results in the following constraint:
(8)    (>(x2[2], 0)=TRUE∧x0[2]=x0[3]∧x1[2]=x1[3]∧x2[2]=x2[3] ⇒ 2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥NonInfC∧2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])∧(U^Increasing(COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥))

We simplified constraint (8) using rule (IV) which results in the following new constraint:
(9)    (>(x2[2], 0)=TRUE ⇒ 2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥NonInfC∧2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])∧(U^Increasing(COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥))

We simplified constraint (9) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(10)    (x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧[(-1)bni_15 + (-1)Bound*bni_15] + [bni_15]x2[2] ≥ 0∧[(-1)bso_16] ≥ 0)

We simplified constraint (10) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(11)    (x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧[(-1)bni_15 + (-1)Bound*bni_15] + [bni_15]x2[2] ≥ 0∧[(-1)bso_16] ≥ 0)

We simplified constraint (11) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(12)    (x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧[(-1)bni_15 + (-1)Bound*bni_15] + [bni_15]x2[2] ≥ 0∧[(-1)bso_16] ≥ 0)

We simplified constraint (12) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(13)    (x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧0 = 0∧0 = 0∧[(-1)bni_15 + (-1)Bound*bni_15] + [bni_15]x2[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_16] ≥ 0)

We simplified constraint (13) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(14)    (x2[2] ≥ 0 ⇒ (U^Increasing(COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_15] + [bni_15]x2[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_16] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))
- (x2[2] ≥ 0 ⇒ (U^Increasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_13] + [bni_13]x2[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_14] ≥ 0)
2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])
- (x2[2] ≥ 0 ⇒ (U^Increasing(COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_15] + [bni_15]x2[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_16] ≥ 0)

POL(TRUE) = 0
POL(FALSE) = 0
POL(COND_2941_0_CREATEMETALIST_LE1(x₁, x₂, x₃, x₄)) = [-1] + x₄
POL(2941_0_CREATEMETALIST_LE(x₁, x₂, x₃)) = [-1] + x₃
POL(+(x₁, x₂)) = x₁ + x₂
POL(-1) = [-1]
POL(>(x₁, x₂)) = [-1]
POL(0) = 0

The following pairs are in P_>:

COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))

The following pairs are in P_bound:

COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))
2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])

The following pairs are in P_≥:

2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])

There are no usable rules.

(13) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(2): 2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(x2[2] > 0, x0[2], x1[2], x2[2])

The set Q is empty.

(14) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(15) TRUE

(16) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: CountMetaList.main([Ljava/lang/String;)V
SCC calls the following helper methods:
Performed SCC analyses: UsedFieldsAnalysis

(17) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 137 rules for P and 0 rules for R.

P rules:
3351_0_countMetaList_NULL(EOS(STATIC_3351), o3582, java.lang.Object(o3590sub), java.lang.Object(o3590sub)) → 3353_0_countMetaList_NULL(EOS(STATIC_3353), o3582, java.lang.Object(o3590sub), java.lang.Object(o3590sub))
3353_0_countMetaList_NULL(EOS(STATIC_3353), o3582, java.lang.Object(o3590sub), java.lang.Object(o3590sub)) → 3355_0_countMetaList_Load(EOS(STATIC_3355), o3582, java.lang.Object(o3590sub))
3355_0_countMetaList_Load(EOS(STATIC_3355), o3582, java.lang.Object(o3590sub)) → 3358_0_countMetaList_FieldAccess(EOS(STATIC_3358), o3582, java.lang.Object(o3590sub), java.lang.Object(o3590sub))
3358_0_countMetaList_FieldAccess(EOS(STATIC_3358), o3582, java.lang.Object(o3590sub), java.lang.Object(o3590sub)) → 3361_0_countMetaList_FieldAccess(EOS(STATIC_3361), o3582, java.lang.Object(o3590sub), java.lang.Object(o3590sub))
3358_0_countMetaList_FieldAccess(EOS(STATIC_3358), java.lang.Object(o3590sub), java.lang.Object(o3590sub), java.lang.Object(o3590sub)) → 3362_0_countMetaList_FieldAccess(EOS(STATIC_3362), java.lang.Object(o3590sub), java.lang.Object(o3590sub), java.lang.Object(o3590sub))
3361_0_countMetaList_FieldAccess(EOS(STATIC_3361), o3582, java.lang.Object(List(EOC, o3592, o3593)), java.lang.Object(List(EOC, o3592, o3593))) → 3365_0_countMetaList_FieldAccess(EOS(STATIC_3365), o3582, java.lang.Object(List(EOC, o3592, o3593)), java.lang.Object(List(EOC, o3592, o3593)))
3365_0_countMetaList_FieldAccess(EOS(STATIC_3365), o3582, java.lang.Object(List(EOC, o3592, o3593)), java.lang.Object(List(EOC, o3592, o3593))) → 3369_0_countMetaList_CheckCast(EOS(STATIC_3369), o3582, java.lang.Object(List(EOC, o3592, o3593)), o3592)
3369_0_countMetaList_CheckCast(EOS(STATIC_3369), o3582, java.lang.Object(List(EOC, java.lang.Object(o3609sub), o3593)), java.lang.Object(o3609sub)) → 3374_0_countMetaList_CheckCast(EOS(STATIC_3374), o3582, java.lang.Object(List(EOC, java.lang.Object(o3609sub), o3593)), java.lang.Object(o3609sub))
3369_0_countMetaList_CheckCast(EOS(STATIC_3369), o3582, java.lang.Object(List(EOC, NULL, o3593)), NULL) → 3375_0_countMetaList_CheckCast(EOS(STATIC_3375), o3582, java.lang.Object(List(EOC, NULL, o3593)), NULL)
3374_0_countMetaList_CheckCast(EOS(STATIC_3374), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub)) → 3380_0_countMetaList_CheckCast(EOS(STATIC_3380), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub))
3374_0_countMetaList_CheckCast(EOS(STATIC_3374), o3582, java.lang.Object(List(EOC, java.lang.Object(o3612sub), o3593)), java.lang.Object(o3612sub)) → 3382_0_countMetaList_CheckCast(EOS(STATIC_3382), o3582, java.lang.Object(List(EOC, java.lang.Object(o3612sub), o3593)), java.lang.Object(o3612sub))
3380_0_countMetaList_CheckCast(EOS(STATIC_3380), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub)) → 3390_0_countMetaList_EQ(EOS(STATIC_3390), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), 1)
3390_0_countMetaList_EQ(EOS(STATIC_3390), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), matching1) → 3407_0_countMetaList_Load(EOS(STATIC_3407), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593))) | &&(>(1, 0), =(matching1, 1))
3407_0_countMetaList_Load(EOS(STATIC_3407), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593))) → 3417_0_countMetaList_FieldAccess(EOS(STATIC_3417), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)))
3417_0_countMetaList_FieldAccess(EOS(STATIC_3417), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593))) → 3429_0_countMetaList_CheckCast(EOS(STATIC_3429), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub))
3429_0_countMetaList_CheckCast(EOS(STATIC_3429), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub)) → 3438_0_countMetaList_Store(EOS(STATIC_3438), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub))
3438_0_countMetaList_Store(EOS(STATIC_3438), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub)) → 3444_0_countMetaList_Load(EOS(STATIC_3444), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub))
3444_0_countMetaList_Load(EOS(STATIC_3444), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub)) → 3450_0_countMetaList_Load(EOS(STATIC_3450), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub), java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)))
3450_0_countMetaList_Load(EOS(STATIC_3450), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub), java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593))) → 3459_0_countMetaList_FieldAccess(EOS(STATIC_3459), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub), java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub))
3459_0_countMetaList_FieldAccess(EOS(STATIC_3459), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub), java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub)) → 3463_0_countMetaList_FieldAccess(EOS(STATIC_3463), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub), java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub))
3459_0_countMetaList_FieldAccess(EOS(STATIC_3459), java.lang.Object(o3611sub), java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub), java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub)) → 3464_0_countMetaList_FieldAccess(EOS(STATIC_3464), java.lang.Object(o3611sub), java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub), java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub))
3463_0_countMetaList_FieldAccess(EOS(STATIC_3463), o3582, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3796, o3797)), o3593)), java.lang.Object(List(EOC, o3796, o3797)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3796, o3797)), o3593)), java.lang.Object(List(EOC, o3796, o3797))) → 3467_0_countMetaList_FieldAccess(EOS(STATIC_3467), o3582, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3796, o3797)), o3593)), java.lang.Object(List(EOC, o3796, o3797)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3796, o3797)), o3593)), java.lang.Object(List(EOC, o3796, o3797)))
3467_0_countMetaList_FieldAccess(EOS(STATIC_3467), o3582, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3796, o3797)), o3593)), java.lang.Object(List(EOC, o3796, o3797)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3796, o3797)), o3593)), java.lang.Object(List(EOC, o3796, o3797))) → 3473_0_countMetaList_FieldAccess(EOS(STATIC_3473), o3582, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3796, o3797)), o3593)), java.lang.Object(List(EOC, o3796, o3797)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3796, o3797)), o3593)), o3797)
3473_0_countMetaList_FieldAccess(EOS(STATIC_3473), o3582, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3796, o3797)), o3593)), java.lang.Object(List(EOC, o3796, o3797)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3796, o3797)), o3593)), o3797) → 3480_0_countMetaList_New(EOS(STATIC_3480), o3582put, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, o3796, o3797)))
3480_0_countMetaList_New(EOS(STATIC_3480), o3582, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, o3796, o3797))) → 3487_0_countMetaList_Duplicate(EOS(STATIC_3487), o3582, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, o3796, o3797)), java.lang.Object(List(EOC, NULL, NULL)))
3487_0_countMetaList_Duplicate(EOS(STATIC_3487), o3582, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, o3796, o3797)), java.lang.Object(List(EOC, NULL, NULL))) → 3493_0_countMetaList_Load(EOS(STATIC_3493), o3582, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, o3796, o3797)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)))
3493_0_countMetaList_Load(EOS(STATIC_3493), o3582, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, o3796, o3797)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL))) → 3501_0_countMetaList_FieldAccess(EOS(STATIC_3501), o3582, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, o3796, o3797)))
3501_0_countMetaList_FieldAccess(EOS(STATIC_3501), o3582, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, o3796, o3797))) → 3508_0_countMetaList_Load(EOS(STATIC_3508), o3582, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3796)
3508_0_countMetaList_Load(EOS(STATIC_3508), o3582, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3796) → 3515_0_countMetaList_InvokeMethod(EOS(STATIC_3515), o3582, java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)))
3515_0_countMetaList_InvokeMethod(EOS(STATIC_3515), o3582, java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593))) → 3520_0_<init>_Load(EOS(STATIC_3520), o3582, java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)))
3520_0_<init>_Load(EOS(STATIC_3520), o3582, java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593))) → 3525_0_<init>_InvokeMethod(EOS(STATIC_3525), o3582, java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)))
3525_0_<init>_InvokeMethod(EOS(STATIC_3525), o3582, java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL))) → 3531_0_<init>_Load(EOS(STATIC_3531), o3582, java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)))
3531_0_<init>_Load(EOS(STATIC_3531), o3582, java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593))) → 3537_0_<init>_Load(EOS(STATIC_3537), o3582, java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)))
3537_0_<init>_Load(EOS(STATIC_3537), o3582, java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL))) → 3543_0_<init>_FieldAccess(EOS(STATIC_3543), o3582, java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3796)
3543_0_<init>_FieldAccess(EOS(STATIC_3543), o3582, java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3796) → 3550_0_<init>_Load(EOS(STATIC_3550), o3582, java.lang.Object(List(EOC, o3796, NULL)), java.lang.Object(List(EOC, o3796, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, o3796, NULL)), java.lang.Object(List(EOC, o3797, o3593)))
3550_0_<init>_Load(EOS(STATIC_3550), o3582, java.lang.Object(List(EOC, o3796, NULL)), java.lang.Object(List(EOC, o3796, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, o3796, NULL)), java.lang.Object(List(EOC, o3797, o3593))) → 3557_0_<init>_Load(EOS(STATIC_3557), o3582, java.lang.Object(List(EOC, o3796, NULL)), java.lang.Object(List(EOC, o3796, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, o3796, NULL)))
3557_0_<init>_Load(EOS(STATIC_3557), o3582, java.lang.Object(List(EOC, o3796, NULL)), java.lang.Object(List(EOC, o3796, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, o3796, NULL))) → 3563_0_<init>_FieldAccess(EOS(STATIC_3563), o3582, java.lang.Object(List(EOC, o3796, NULL)), java.lang.Object(List(EOC, o3796, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, o3796, NULL)), java.lang.Object(List(EOC, o3797, o3593)))
3563_0_<init>_FieldAccess(EOS(STATIC_3563), o3582, java.lang.Object(List(EOC, o3796, NULL)), java.lang.Object(List(EOC, o3796, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, o3796, NULL)), java.lang.Object(List(EOC, o3797, o3593))) → 3571_0_<init>_Return(EOS(STATIC_3571), o3582, java.lang.Object(List(EOC, o3796, java.lang.Object(List(EOC, o3797, o3593)))), java.lang.Object(List(EOC, o3796, java.lang.Object(List(EOC, o3797, o3593)))), o3796, java.lang.Object(List(EOC, o3797, o3593)))
3571_0_<init>_Return(EOS(STATIC_3571), o3582, java.lang.Object(List(EOC, o3796, java.lang.Object(List(EOC, o3797, o3593)))), java.lang.Object(List(EOC, o3796, java.lang.Object(List(EOC, o3797, o3593)))), o3796, java.lang.Object(List(EOC, o3797, o3593))) → 3579_0_countMetaList_Store(EOS(STATIC_3579), o3582, java.lang.Object(List(EOC, o3796, java.lang.Object(List(EOC, o3797, o3593)))))
3579_0_countMetaList_Store(EOS(STATIC_3579), o3582, java.lang.Object(List(EOC, o3796, java.lang.Object(List(EOC, o3797, o3593))))) → 3589_0_countMetaList_Load(EOS(STATIC_3589), o3582, java.lang.Object(List(EOC, o3796, java.lang.Object(List(EOC, o3797, o3593)))))
3589_0_countMetaList_Load(EOS(STATIC_3589), o3582, java.lang.Object(List(EOC, o3796, java.lang.Object(List(EOC, o3797, o3593))))) → 3601_0_countMetaList_FieldAccess(EOS(STATIC_3601), o3582, java.lang.Object(List(EOC, o3796, java.lang.Object(List(EOC, o3797, o3593)))))
3601_0_countMetaList_FieldAccess(EOS(STATIC_3601), o3582, java.lang.Object(List(EOC, o3796, java.lang.Object(List(EOC, o3797, o3593))))) → 3610_0_countMetaList_Store(EOS(STATIC_3610), o3582, java.lang.Object(List(EOC, o3797, o3593)))
3610_0_countMetaList_Store(EOS(STATIC_3610), o3582, java.lang.Object(List(EOC, o3797, o3593))) → 3617_0_countMetaList_Inc(EOS(STATIC_3617), o3582, java.lang.Object(List(EOC, o3797, o3593)))
3617_0_countMetaList_Inc(EOS(STATIC_3617), o3582, java.lang.Object(List(EOC, o3797, o3593))) → 3625_0_countMetaList_JMP(EOS(STATIC_3625), o3582, java.lang.Object(List(EOC, o3797, o3593)))
3625_0_countMetaList_JMP(EOS(STATIC_3625), o3582, java.lang.Object(List(EOC, o3797, o3593))) → 3633_0_countMetaList_Load(EOS(STATIC_3633), o3582, java.lang.Object(List(EOC, o3797, o3593)))
3633_0_countMetaList_Load(EOS(STATIC_3633), o3582, java.lang.Object(List(EOC, o3797, o3593))) → 3348_0_countMetaList_Load(EOS(STATIC_3348), o3582, java.lang.Object(List(EOC, o3797, o3593)))
3348_0_countMetaList_Load(EOS(STATIC_3348), o3582, o3581) → 3351_0_countMetaList_NULL(EOS(STATIC_3351), o3582, o3581, o3581)
3464_0_countMetaList_FieldAccess(EOS(STATIC_3464), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3799, o3800)), o3593)), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3799, o3800)), o3593)), java.lang.Object(List(EOC, o3799, o3800))) → 3469_0_countMetaList_FieldAccess(EOS(STATIC_3469), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3799, o3800)), o3593)), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3799, o3800)), o3593)), java.lang.Object(List(EOC, o3799, o3800)))
3469_0_countMetaList_FieldAccess(EOS(STATIC_3469), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3799, o3800)), o3593)), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3799, o3800)), o3593)), java.lang.Object(List(EOC, o3799, o3800))) → 3476_0_countMetaList_FieldAccess(EOS(STATIC_3476), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3799, o3800)), o3593)), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3799, o3800)), o3593)), o3800)
3476_0_countMetaList_FieldAccess(EOS(STATIC_3476), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3799, o3800)), o3593)), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3799, o3800)), o3593)), o3800) → 3483_0_countMetaList_New(EOS(STATIC_3483), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, o3799, o3800)))
3483_0_countMetaList_New(EOS(STATIC_3483), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, o3799, o3800))) → 3490_0_countMetaList_Duplicate(EOS(STATIC_3490), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, NULL, NULL)))
3490_0_countMetaList_Duplicate(EOS(STATIC_3490), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, NULL, NULL))) → 3497_0_countMetaList_Load(EOS(STATIC_3497), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)))
3497_0_countMetaList_Load(EOS(STATIC_3497), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL))) → 3504_0_countMetaList_FieldAccess(EOS(STATIC_3504), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, o3799, o3800)))
3504_0_countMetaList_FieldAccess(EOS(STATIC_3504), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, o3799, o3800))) → 3511_0_countMetaList_Load(EOS(STATIC_3511), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3799)
3511_0_countMetaList_Load(EOS(STATIC_3511), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3799) → 3517_0_countMetaList_InvokeMethod(EOS(STATIC_3517), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)))
3517_0_countMetaList_InvokeMethod(EOS(STATIC_3517), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593))) → 3521_0_<init>_Load(EOS(STATIC_3521), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)))
3521_0_<init>_Load(EOS(STATIC_3521), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593))) → 3528_0_<init>_InvokeMethod(EOS(STATIC_3528), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)))
3528_0_<init>_InvokeMethod(EOS(STATIC_3528), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL))) → 3533_0_<init>_Load(EOS(STATIC_3533), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)))
3533_0_<init>_Load(EOS(STATIC_3533), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593))) → 3540_0_<init>_Load(EOS(STATIC_3540), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)))
3540_0_<init>_Load(EOS(STATIC_3540), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL))) → 3546_0_<init>_FieldAccess(EOS(STATIC_3546), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3799)
3546_0_<init>_FieldAccess(EOS(STATIC_3546), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3799) → 3554_0_<init>_Load(EOS(STATIC_3554), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3799, NULL)), java.lang.Object(List(EOC, o3799, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, o3799, NULL)), java.lang.Object(List(EOC, o3800, o3593)))
3554_0_<init>_Load(EOS(STATIC_3554), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3799, NULL)), java.lang.Object(List(EOC, o3799, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, o3799, NULL)), java.lang.Object(List(EOC, o3800, o3593))) → 3559_0_<init>_Load(EOS(STATIC_3559), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3799, NULL)), java.lang.Object(List(EOC, o3799, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, o3799, NULL)))
3559_0_<init>_Load(EOS(STATIC_3559), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3799, NULL)), java.lang.Object(List(EOC, o3799, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, o3799, NULL))) → 3565_0_<init>_FieldAccess(EOS(STATIC_3565), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3799, NULL)), java.lang.Object(List(EOC, o3799, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, o3799, NULL)), java.lang.Object(List(EOC, o3800, o3593)))
3565_0_<init>_FieldAccess(EOS(STATIC_3565), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3799, NULL)), java.lang.Object(List(EOC, o3799, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, o3799, NULL)), java.lang.Object(List(EOC, o3800, o3593))) → 3575_0_<init>_Return(EOS(STATIC_3575), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3799, java.lang.Object(List(EOC, o3800, o3593)))), java.lang.Object(List(EOC, o3799, java.lang.Object(List(EOC, o3800, o3593)))), o3799, java.lang.Object(List(EOC, o3800, o3593)))
3575_0_<init>_Return(EOS(STATIC_3575), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3799, java.lang.Object(List(EOC, o3800, o3593)))), java.lang.Object(List(EOC, o3799, java.lang.Object(List(EOC, o3800, o3593)))), o3799, java.lang.Object(List(EOC, o3800, o3593))) → 3582_0_countMetaList_Store(EOS(STATIC_3582), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3799, java.lang.Object(List(EOC, o3800, o3593)))))
3582_0_countMetaList_Store(EOS(STATIC_3582), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3799, java.lang.Object(List(EOC, o3800, o3593))))) → 3594_0_countMetaList_Load(EOS(STATIC_3594), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3799, java.lang.Object(List(EOC, o3800, o3593)))))
3594_0_countMetaList_Load(EOS(STATIC_3594), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3799, java.lang.Object(List(EOC, o3800, o3593))))) → 3606_0_countMetaList_FieldAccess(EOS(STATIC_3606), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3799, java.lang.Object(List(EOC, o3800, o3593)))))
3606_0_countMetaList_FieldAccess(EOS(STATIC_3606), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3799, java.lang.Object(List(EOC, o3800, o3593))))) → 3613_0_countMetaList_Store(EOS(STATIC_3613), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)))
3613_0_countMetaList_Store(EOS(STATIC_3613), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593))) → 3620_0_countMetaList_Inc(EOS(STATIC_3620), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)))
3620_0_countMetaList_Inc(EOS(STATIC_3620), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593))) → 3627_0_countMetaList_JMP(EOS(STATIC_3627), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)))
3627_0_countMetaList_JMP(EOS(STATIC_3627), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593))) → 3635_0_countMetaList_Load(EOS(STATIC_3635), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)))
3635_0_countMetaList_Load(EOS(STATIC_3635), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593))) → 3348_0_countMetaList_Load(EOS(STATIC_3348), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)))
3382_0_countMetaList_CheckCast(EOS(STATIC_3382), o3582, java.lang.Object(List(EOC, java.lang.Object(o3612sub), o3593)), java.lang.Object(o3612sub)) → 3395_0_countMetaList_EQ(EOS(STATIC_3395), o3582, java.lang.Object(List(EOC, java.lang.Object(o3612sub), o3593)), 0)
3395_0_countMetaList_EQ(EOS(STATIC_3395), o3582, java.lang.Object(List(EOC, java.lang.Object(o3612sub), o3593)), matching1) → 3409_0_countMetaList_Load(EOS(STATIC_3409), o3582, java.lang.Object(List(EOC, java.lang.Object(o3612sub), o3593))) | =(matching1, 0)
3409_0_countMetaList_Load(EOS(STATIC_3409), o3582, java.lang.Object(List(EOC, java.lang.Object(o3612sub), o3593))) → 3420_0_countMetaList_FieldAccess(EOS(STATIC_3420), o3582, java.lang.Object(List(EOC, java.lang.Object(o3612sub), o3593)))
3420_0_countMetaList_FieldAccess(EOS(STATIC_3420), o3582, java.lang.Object(List(EOC, java.lang.Object(o3612sub), o3593))) → 3432_0_countMetaList_Store(EOS(STATIC_3432), o3582, o3593)
3432_0_countMetaList_Store(EOS(STATIC_3432), o3582, o3593) → 3439_0_countMetaList_Inc(EOS(STATIC_3439), o3582, o3593)
3439_0_countMetaList_Inc(EOS(STATIC_3439), o3582, o3593) → 3445_0_countMetaList_JMP(EOS(STATIC_3445), o3582, o3593)
3445_0_countMetaList_JMP(EOS(STATIC_3445), o3582, o3593) → 3453_0_countMetaList_Load(EOS(STATIC_3453), o3582, o3593)
3453_0_countMetaList_Load(EOS(STATIC_3453), o3582, o3593) → 3348_0_countMetaList_Load(EOS(STATIC_3348), o3582, o3593)
3375_0_countMetaList_CheckCast(EOS(STATIC_3375), o3582, java.lang.Object(List(EOC, NULL, o3593)), NULL) → 3383_0_countMetaList_EQ(EOS(STATIC_3383), o3582, java.lang.Object(List(EOC, NULL, o3593)), 0)
3383_0_countMetaList_EQ(EOS(STATIC_3383), o3582, java.lang.Object(List(EOC, NULL, o3593)), matching1) → 3396_0_countMetaList_Load(EOS(STATIC_3396), o3582, java.lang.Object(List(EOC, NULL, o3593))) | =(matching1, 0)
3396_0_countMetaList_Load(EOS(STATIC_3396), o3582, java.lang.Object(List(EOC, NULL, o3593))) → 3410_0_countMetaList_FieldAccess(EOS(STATIC_3410), o3582, java.lang.Object(List(EOC, NULL, o3593)))
3410_0_countMetaList_FieldAccess(EOS(STATIC_3410), o3582, java.lang.Object(List(EOC, NULL, o3593))) → 3421_0_countMetaList_Store(EOS(STATIC_3421), o3582, o3593)
3421_0_countMetaList_Store(EOS(STATIC_3421), o3582, o3593) → 3432_0_countMetaList_Store(EOS(STATIC_3432), o3582, o3593)
3362_0_countMetaList_FieldAccess(EOS(STATIC_3362), java.lang.Object(List(EOC, o3595, o3596)), java.lang.Object(List(EOC, o3595, o3596)), java.lang.Object(List(EOC, o3595, o3596))) → 3366_0_countMetaList_FieldAccess(EOS(STATIC_3366), java.lang.Object(List(EOC, o3595, o3596)), java.lang.Object(List(EOC, o3595, o3596)), java.lang.Object(List(EOC, o3595, o3596)))
3366_0_countMetaList_FieldAccess(EOS(STATIC_3366), java.lang.Object(List(EOC, o3595, o3596)), java.lang.Object(List(EOC, o3595, o3596)), java.lang.Object(List(EOC, o3595, o3596))) → 3372_0_countMetaList_CheckCast(EOS(STATIC_3372), java.lang.Object(List(EOC, o3595, o3596)), java.lang.Object(List(EOC, o3595, o3596)), o3595)
3372_0_countMetaList_CheckCast(EOS(STATIC_3372), java.lang.Object(List(EOC, java.lang.Object(o3610sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3610sub), o3596)), java.lang.Object(o3610sub)) → 3377_0_countMetaList_CheckCast(EOS(STATIC_3377), java.lang.Object(List(EOC, java.lang.Object(o3610sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3610sub), o3596)), java.lang.Object(o3610sub))
3372_0_countMetaList_CheckCast(EOS(STATIC_3372), java.lang.Object(List(EOC, NULL, o3596)), java.lang.Object(List(EOC, NULL, o3596)), NULL) → 3378_0_countMetaList_CheckCast(EOS(STATIC_3378), java.lang.Object(List(EOC, NULL, o3596)), java.lang.Object(List(EOC, NULL, o3596)), NULL)
3377_0_countMetaList_CheckCast(EOS(STATIC_3377), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(o3613sub)) → 3386_0_countMetaList_CheckCast(EOS(STATIC_3386), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(o3613sub))
3377_0_countMetaList_CheckCast(EOS(STATIC_3377), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), java.lang.Object(o3614sub)) → 3387_0_countMetaList_CheckCast(EOS(STATIC_3387), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), java.lang.Object(o3614sub))
3386_0_countMetaList_CheckCast(EOS(STATIC_3386), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(o3613sub)) → 3399_0_countMetaList_EQ(EOS(STATIC_3399), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), 1)
3399_0_countMetaList_EQ(EOS(STATIC_3399), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), matching1) → 3412_0_countMetaList_Load(EOS(STATIC_3412), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596))) | &&(>(1, 0), =(matching1, 1))
3412_0_countMetaList_Load(EOS(STATIC_3412), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596))) → 3423_0_countMetaList_FieldAccess(EOS(STATIC_3423), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)))
3423_0_countMetaList_FieldAccess(EOS(STATIC_3423), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596))) → 3435_0_countMetaList_CheckCast(EOS(STATIC_3435), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(o3613sub))
3435_0_countMetaList_CheckCast(EOS(STATIC_3435), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(o3613sub)) → 3441_0_countMetaList_Store(EOS(STATIC_3441), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(o3613sub))
3441_0_countMetaList_Store(EOS(STATIC_3441), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(o3613sub)) → 3447_0_countMetaList_Load(EOS(STATIC_3447), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(o3613sub))
3447_0_countMetaList_Load(EOS(STATIC_3447), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(o3613sub)) → 3455_0_countMetaList_Load(EOS(STATIC_3455), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(o3613sub), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)))
3455_0_countMetaList_Load(EOS(STATIC_3455), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(o3613sub), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596))) → 3462_0_countMetaList_FieldAccess(EOS(STATIC_3462), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(o3613sub), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(o3613sub))
3462_0_countMetaList_FieldAccess(EOS(STATIC_3462), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3793, o3794)), o3596)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3793, o3794)), o3596)), java.lang.Object(List(EOC, o3793, o3794)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3793, o3794)), o3596)), java.lang.Object(List(EOC, o3793, o3794))) → 3466_0_countMetaList_FieldAccess(EOS(STATIC_3466), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3793, o3794)), o3596)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3793, o3794)), o3596)), java.lang.Object(List(EOC, o3793, o3794)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3793, o3794)), o3596)), java.lang.Object(List(EOC, o3793, o3794)))
3466_0_countMetaList_FieldAccess(EOS(STATIC_3466), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3793, o3794)), o3596)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3793, o3794)), o3596)), java.lang.Object(List(EOC, o3793, o3794)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3793, o3794)), o3596)), java.lang.Object(List(EOC, o3793, o3794))) → 3470_0_countMetaList_FieldAccess(EOS(STATIC_3470), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3793, o3794)), o3596)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3793, o3794)), o3596)), java.lang.Object(List(EOC, o3793, o3794)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3793, o3794)), o3596)), o3794)
3470_0_countMetaList_FieldAccess(EOS(STATIC_3470), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3793, o3794)), o3596)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3793, o3794)), o3596)), java.lang.Object(List(EOC, o3793, o3794)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3793, o3794)), o3596)), o3794) → 3477_0_countMetaList_New(EOS(STATIC_3477), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, o3794)))
3477_0_countMetaList_New(EOS(STATIC_3477), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, o3794))) → 3485_0_countMetaList_Duplicate(EOS(STATIC_3485), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, o3794)), java.lang.Object(List(EOC, NULL, NULL)))
3485_0_countMetaList_Duplicate(EOS(STATIC_3485), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, o3794)), java.lang.Object(List(EOC, NULL, NULL))) → 3491_0_countMetaList_Load(EOS(STATIC_3491), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, o3794)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)))
3491_0_countMetaList_Load(EOS(STATIC_3491), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, o3794)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL))) → 3498_0_countMetaList_FieldAccess(EOS(STATIC_3498), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, o3793, o3794)))
3498_0_countMetaList_FieldAccess(EOS(STATIC_3498), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, o3793, o3794))) → 3505_0_countMetaList_Load(EOS(STATIC_3505), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3793)
3505_0_countMetaList_Load(EOS(STATIC_3505), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3793) → 3512_0_countMetaList_InvokeMethod(EOS(STATIC_3512), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)))
3512_0_countMetaList_InvokeMethod(EOS(STATIC_3512), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596))) → 3518_0_<init>_Load(EOS(STATIC_3518), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)))
3518_0_<init>_Load(EOS(STATIC_3518), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596))) → 3523_0_<init>_InvokeMethod(EOS(STATIC_3523), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)))
3523_0_<init>_InvokeMethod(EOS(STATIC_3523), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL))) → 3530_0_<init>_Load(EOS(STATIC_3530), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)))
3530_0_<init>_Load(EOS(STATIC_3530), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596))) → 3535_0_<init>_Load(EOS(STATIC_3535), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)))
3535_0_<init>_Load(EOS(STATIC_3535), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL))) → 3541_0_<init>_FieldAccess(EOS(STATIC_3541), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), o3793)
3541_0_<init>_FieldAccess(EOS(STATIC_3541), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), o3793) → 3548_0_<init>_Load(EOS(STATIC_3548), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, NULL)), java.lang.Object(List(EOC, o3793, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, NULL)), java.lang.Object(List(EOC, o3794, o3596)))
3548_0_<init>_Load(EOS(STATIC_3548), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, NULL)), java.lang.Object(List(EOC, o3793, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, NULL)), java.lang.Object(List(EOC, o3794, o3596))) → 3555_0_<init>_Load(EOS(STATIC_3555), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, NULL)), java.lang.Object(List(EOC, o3793, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, NULL)))
3555_0_<init>_Load(EOS(STATIC_3555), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, NULL)), java.lang.Object(List(EOC, o3793, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, NULL))) → 3561_0_<init>_FieldAccess(EOS(STATIC_3561), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, NULL)), java.lang.Object(List(EOC, o3793, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, NULL)), java.lang.Object(List(EOC, o3794, o3596)))
3561_0_<init>_FieldAccess(EOS(STATIC_3561), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, NULL)), java.lang.Object(List(EOC, o3793, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, NULL)), java.lang.Object(List(EOC, o3794, o3596))) → 3568_0_<init>_Return(EOS(STATIC_3568), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, java.lang.Object(List(EOC, o3794, o3596)))), java.lang.Object(List(EOC, o3793, java.lang.Object(List(EOC, o3794, o3596)))), o3793, java.lang.Object(List(EOC, o3794, o3596)))
3568_0_<init>_Return(EOS(STATIC_3568), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, java.lang.Object(List(EOC, o3794, o3596)))), java.lang.Object(List(EOC, o3793, java.lang.Object(List(EOC, o3794, o3596)))), o3793, java.lang.Object(List(EOC, o3794, o3596))) → 3576_0_countMetaList_Store(EOS(STATIC_3576), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, java.lang.Object(List(EOC, o3794, o3596)))))
3576_0_countMetaList_Store(EOS(STATIC_3576), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, java.lang.Object(List(EOC, o3794, o3596))))) → 3585_0_countMetaList_Load(EOS(STATIC_3585), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, java.lang.Object(List(EOC, o3794, o3596)))))
3585_0_countMetaList_Load(EOS(STATIC_3585), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, java.lang.Object(List(EOC, o3794, o3596))))) → 3597_0_countMetaList_FieldAccess(EOS(STATIC_3597), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, java.lang.Object(List(EOC, o3794, o3596)))))
3597_0_countMetaList_FieldAccess(EOS(STATIC_3597), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, java.lang.Object(List(EOC, o3794, o3596))))) → 3608_0_countMetaList_Store(EOS(STATIC_3608), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)))
3608_0_countMetaList_Store(EOS(STATIC_3608), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596))) → 3615_0_countMetaList_Inc(EOS(STATIC_3615), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)))
3615_0_countMetaList_Inc(EOS(STATIC_3615), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596))) → 3622_0_countMetaList_JMP(EOS(STATIC_3622), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)))
3622_0_countMetaList_JMP(EOS(STATIC_3622), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596))) → 3630_0_countMetaList_Load(EOS(STATIC_3630), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)))
3630_0_countMetaList_Load(EOS(STATIC_3630), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596))) → 3348_0_countMetaList_Load(EOS(STATIC_3348), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)))
3387_0_countMetaList_CheckCast(EOS(STATIC_3387), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), java.lang.Object(o3614sub)) → 3404_0_countMetaList_EQ(EOS(STATIC_3404), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), 0)
3404_0_countMetaList_EQ(EOS(STATIC_3404), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), matching1) → 3415_0_countMetaList_Load(EOS(STATIC_3415), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596))) | =(matching1, 0)
3415_0_countMetaList_Load(EOS(STATIC_3415), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596))) → 3426_0_countMetaList_FieldAccess(EOS(STATIC_3426), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)))
3426_0_countMetaList_FieldAccess(EOS(STATIC_3426), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596))) → 3437_0_countMetaList_Store(EOS(STATIC_3437), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), o3596)
3437_0_countMetaList_Store(EOS(STATIC_3437), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), o3596) → 3442_0_countMetaList_Inc(EOS(STATIC_3442), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), o3596)
3442_0_countMetaList_Inc(EOS(STATIC_3442), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), o3596) → 3449_0_countMetaList_JMP(EOS(STATIC_3449), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), o3596)
3449_0_countMetaList_JMP(EOS(STATIC_3449), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), o3596) → 3457_0_countMetaList_Load(EOS(STATIC_3457), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), o3596)
3457_0_countMetaList_Load(EOS(STATIC_3457), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), o3596) → 3348_0_countMetaList_Load(EOS(STATIC_3348), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), o3596)
3378_0_countMetaList_CheckCast(EOS(STATIC_3378), java.lang.Object(List(EOC, NULL, o3596)), java.lang.Object(List(EOC, NULL, o3596)), NULL) → 3388_0_countMetaList_EQ(EOS(STATIC_3388), java.lang.Object(List(EOC, NULL, o3596)), java.lang.Object(List(EOC, NULL, o3596)), 0)
3388_0_countMetaList_EQ(EOS(STATIC_3388), java.lang.Object(List(EOC, NULL, o3596)), java.lang.Object(List(EOC, NULL, o3596)), matching1) → 3406_0_countMetaList_Load(EOS(STATIC_3406), java.lang.Object(List(EOC, NULL, o3596)), java.lang.Object(List(EOC, NULL, o3596))) | =(matching1, 0)
3406_0_countMetaList_Load(EOS(STATIC_3406), java.lang.Object(List(EOC, NULL, o3596)), java.lang.Object(List(EOC, NULL, o3596))) → 3416_0_countMetaList_FieldAccess(EOS(STATIC_3416), java.lang.Object(List(EOC, NULL, o3596)), java.lang.Object(List(EOC, NULL, o3596)))
3416_0_countMetaList_FieldAccess(EOS(STATIC_3416), java.lang.Object(List(EOC, NULL, o3596)), java.lang.Object(List(EOC, NULL, o3596))) → 3427_0_countMetaList_Store(EOS(STATIC_3427), java.lang.Object(List(EOC, NULL, o3596)), o3596)
3427_0_countMetaList_Store(EOS(STATIC_3427), java.lang.Object(List(EOC, NULL, o3596)), o3596) → 3432_0_countMetaList_Store(EOS(STATIC_3432), java.lang.Object(List(EOC, NULL, o3596)), o3596)
R rules:

Combined rules. Obtained 7 conditional rules for P and 0 conditional rules for R.

P rules:
3351_0_countMetaList_NULL(EOS(STATIC_3351), x0, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x1, x2)), x3)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x1, x2)), x3))) → 3351_0_countMetaList_NULL(EOS(STATIC_3351), x4, java.lang.Object(List(EOC, x2, x3)), java.lang.Object(List(EOC, x2, x3)))
3351_0_countMetaList_NULL(EOS(STATIC_3351), java.lang.Object(List(EOC, x0, x1)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0, x1)), x2)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0, x1)), x2))) → 3351_0_countMetaList_NULL(EOS(STATIC_3351), java.lang.Object(List(EOC, x0, x1)), java.lang.Object(List(EOC, x1, x2)), java.lang.Object(List(EOC, x1, x2)))
3351_0_countMetaList_NULL(EOS(STATIC_3351), x0, java.lang.Object(List(EOC, java.lang.Object(x1), x2)), java.lang.Object(List(EOC, java.lang.Object(x1), x2))) → 3351_0_countMetaList_NULL(EOS(STATIC_3351), x0, x2, x2)
3351_0_countMetaList_NULL(EOS(STATIC_3351), x0, java.lang.Object(List(EOC, NULL, x1)), java.lang.Object(List(EOC, NULL, x1))) → 3351_0_countMetaList_NULL(EOS(STATIC_3351), x0, x1, x1)
3351_0_countMetaList_NULL(EOS(STATIC_3351), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0, x1)), x2)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0, x1)), x2)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0, x1)), x2))) → 3351_0_countMetaList_NULL(EOS(STATIC_3351), java.lang.Object(List(EOC, x1, x2)), java.lang.Object(List(EOC, x1, x2)), java.lang.Object(List(EOC, x1, x2)))
3351_0_countMetaList_NULL(EOS(STATIC_3351), java.lang.Object(List(EOC, java.lang.Object(x0), x1)), java.lang.Object(List(EOC, java.lang.Object(x0), x1)), java.lang.Object(List(EOC, java.lang.Object(x0), x1))) → 3351_0_countMetaList_NULL(EOS(STATIC_3351), java.lang.Object(List(EOC, java.lang.Object(x0), x1)), x1, x1)
3351_0_countMetaList_NULL(EOS(STATIC_3351), java.lang.Object(List(EOC, NULL, x0)), java.lang.Object(List(EOC, NULL, x0)), java.lang.Object(List(EOC, NULL, x0))) → 3351_0_countMetaList_NULL(EOS(STATIC_3351), java.lang.Object(List(EOC, NULL, x0)), x0, x0)
R rules:

Filtered ground terms:

3351_0_countMetaList_NULL(x1, x2, x3, x4) → 3351_0_countMetaList_NULL(x2, x3, x4)
List(x1, x2, x3) → List(x2, x3)
EOS(x1) → EOS

Filtered duplicate args:

3351_0_countMetaList_NULL(x1, x2, x3) → 3351_0_countMetaList_NULL(x1, x3)

Filtered all free variables in P and R:

3351_0_countMetaList_NULL(x1, x2) → 3351_0_countMetaList_NULL(x2)

Current set of rules:

P rules:
3351_0_countMetaList_NULL(java.lang.Object(List(java.lang.Object(List(x1, x2)), x3))) → 3351_0_countMetaList_NULL(java.lang.Object(List(x2, x3)))
3351_0_countMetaList_NULL(java.lang.Object(List(java.lang.Object(x1), x2))) → 3351_0_countMetaList_NULL(x2)
3351_0_countMetaList_NULL(java.lang.Object(List(NULL, x1))) → 3351_0_countMetaList_NULL(x1)
R rules:

Combined rules. Obtained 3 conditional rules for P and 0 conditional rules for R.

Finished conversion. Obtained 3 rules for P and 0 rules for R. System has no predefined symbols.

P rules:
3351_0_COUNTMETALIST_NULL(java.lang.Object(List(java.lang.Object(List(x1, x2)), x3))) → 3351_0_COUNTMETALIST_NULL(java.lang.Object(List(x2, x3)))
3351_0_COUNTMETALIST_NULL(java.lang.Object(List(java.lang.Object(x1), x2))) → 3351_0_COUNTMETALIST_NULL(x2)
3351_0_COUNTMETALIST_NULL(java.lang.Object(List(NULL, x1))) → 3351_0_COUNTMETALIST_NULL(x1)
R rules:

(18) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:
none

R is empty.

The integer pair graph contains the following rules and edges:
(0): 3351_0_COUNTMETALIST_NULL(java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0]))) → 3351_0_COUNTMETALIST_NULL(java.lang.Object(List(x2[0], x3[0])))
(1): 3351_0_COUNTMETALIST_NULL(java.lang.Object(List(java.lang.Object(x1[1]), x2[1]))) → 3351_0_COUNTMETALIST_NULL(x2[1])
(2): 3351_0_COUNTMETALIST_NULL(java.lang.Object(List(NULL, x1[2]))) → 3351_0_COUNTMETALIST_NULL(x1[2])

(0) -> (0), if (java.lang.Object(List(x2[0], x3[0])) →^* java.lang.Object(List(java.lang.Object(List(x1[0]', x2[0]')), x3[0]')))

(0) -> (1), if (java.lang.Object(List(x2[0], x3[0])) →^* java.lang.Object(List(java.lang.Object(x1[1]), x2[1])))

(0) -> (2), if (java.lang.Object(List(x2[0], x3[0])) →^* java.lang.Object(List(NULL, x1[2])))

(1) -> (0), if (x2[1] →^* java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0])))

(1) -> (1), if (x2[1] →^* java.lang.Object(List(java.lang.Object(x1[1]'), x2[1]')))

(1) -> (2), if (x2[1] →^* java.lang.Object(List(NULL, x1[2])))

(2) -> (0), if (x1[2] →^* java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0])))

(2) -> (1), if (x1[2] →^* java.lang.Object(List(java.lang.Object(x1[1]), x2[1])))

(2) -> (2), if (x1[2] →^* java.lang.Object(List(NULL, x1[2]')))

The set Q is empty.

(19) IDPtoQDPProof (SOUND transformation)

Represented integers and predefined function symbols by Terms

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

3351_0_COUNTMETALIST_NULL(java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0]))) → 3351_0_COUNTMETALIST_NULL(java.lang.Object(List(x2[0], x3[0])))
3351_0_COUNTMETALIST_NULL(java.lang.Object(List(java.lang.Object(x1[1]), x2[1]))) → 3351_0_COUNTMETALIST_NULL(x2[1])
3351_0_COUNTMETALIST_NULL(java.lang.Object(List(NULL, x1[2]))) → 3351_0_COUNTMETALIST_NULL(x1[2])

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(21) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

3351_0_COUNTMETALIST_NULL(java.lang.Object(List(NULL, x1[2]))) → 3351_0_COUNTMETALIST_NULL(x1[2])

No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(3351_0_COUNTMETALIST_NULL(x₁)) = 2·x₁
POL(List(x₁, x₂)) = x₁ + 2·x₂
POL(NULL) = 0
POL(java.lang.Object(x₁)) = 2·x₁

(22) Obligation:

Q DP problem:
The TRS P consists of the following rules:

3351_0_COUNTMETALIST_NULL(java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0]))) → 3351_0_COUNTMETALIST_NULL(java.lang.Object(List(x2[0], x3[0])))
3351_0_COUNTMETALIST_NULL(java.lang.Object(List(java.lang.Object(x1[1]), x2[1]))) → 3351_0_COUNTMETALIST_NULL(x2[1])

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(23) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

3351_0_COUNTMETALIST_NULL(java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0]))) → 3351_0_COUNTMETALIST_NULL(java.lang.Object(List(x2[0], x3[0])))
3351_0_COUNTMETALIST_NULL(java.lang.Object(List(java.lang.Object(x1[1]), x2[1]))) → 3351_0_COUNTMETALIST_NULL(x2[1])

Used ordering: Knuth-Bendix order [KBO] with precedence:

List₂ > java.lang.Object₁ > 3351_{0_{COUNTMETALIST_NULL₁}}

and weight map:

3351_0_COUNTMETALIST_NULL_1=1
java.lang.Object_1=1
List_2=0

The variable weight is 1

(24) Obligation:

Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(25) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(0) Obligation:

(1) JBCToGraph (SOUND transformation)

(2) Obligation:

(3) TerminationGraphToSCCProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) SCCToIDPv1Proof (SOUND transformation)

(7) Obligation:

(8) IDPNonInfProof (SOUND transformation)

(9) Obligation:

(10) IDependencyGraphProof (EQUIVALENT transformation)

(11) Obligation:

(12) IDPNonInfProof (SOUND transformation)

(13) Obligation:

(14) IDependencyGraphProof (EQUIVALENT transformation)

(15) TRUE

(16) Obligation:

(17) SCCToIDPv1Proof (SOUND transformation)

(18) Obligation:

(19) IDPtoQDPProof (SOUND transformation)

(20) Obligation:

(21) UsableRulesReductionPairsProof (EQUIVALENT transformation)

(22) Obligation:

(23) MRRProof (EQUIVALENT transformation)

(24) Obligation:

(25) PisEmptyProof (EQUIVALENT transformation)

(26) YES